Problem: f(s(X),X) -> f(X,a(X)) f(X,c(X)) -> f(s(X),X) f(X,X) -> c(X) Proof: Complexity Transformation Processor: strict: f(s(X),X) -> f(X,a(X)) f(X,c(X)) -> f(s(X),X) f(X,X) -> c(X) weak: Matrix Interpretation Processor: dimension: 1 max_matrix: 1 interpretation: [c](x0) = x0 + 32, [a](x0) = x0 + 1, [f](x0, x1) = x0 + x1 + 127, [s](x0) = x0 + 1 orientation: f(s(X),X) = 2X + 128 >= 2X + 128 = f(X,a(X)) f(X,c(X)) = 2X + 159 >= 2X + 128 = f(s(X),X) f(X,X) = 2X + 127 >= X + 32 = c(X) problem: strict: f(s(X),X) -> f(X,a(X)) weak: f(X,c(X)) -> f(s(X),X) f(X,X) -> c(X) Matrix Interpretation Processor: dimension: 1 max_matrix: 1 interpretation: [c](x0) = x0 + 96, [a](x0) = x0 + 64, [f](x0, x1) = x0 + x1 + 96, [s](x0) = x0 + 96 orientation: f(s(X),X) = 2X + 192 >= 2X + 160 = f(X,a(X)) f(X,c(X)) = 2X + 192 >= 2X + 192 = f(s(X),X) f(X,X) = 2X + 96 >= X + 96 = c(X) problem: strict: weak: f(s(X),X) -> f(X,a(X)) f(X,c(X)) -> f(s(X),X) f(X,X) -> c(X) Qed